SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Certifying algorithm</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Certifying algorithm</span></span>

</h1>

</header>

<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="en" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr"><p>In <a href="Theoretical_computer_science" title="Theoretical computer science">theoretical computer science</a>, a <b>certifying algorithm</b> is an algorithm that outputs, together with a solution to the problem it solves, a proof that the solution is correct. A certifying algorithm is said to be <i>efficient</i> if the combined runtime of the algorithm and a <a href="Proof_checker" class="mw-redirect" title="Proof checker">proof checker</a> is slower by at most a constant factor than the best known non-certifying algorithm for the same problem.<sup id="cite_ref-mmns_1-0" class="reference"><a href="#cite_note-mmns-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup>

</p><p>The proof produced by a certifying algorithm should be in some sense simpler than the algorithm itself, for otherwise any algorithm could be considered certifying (with its output verified by running the same algorithm again). Sometimes this is formalized by requiring that a verification of the proof take less time than the original algorithm, while for other problems (in particular those for which the solution can be found in <a href="Linear_time" class="mw-redirect" title="Linear time">linear time</a>) simplicity of the output proof is considered in a less formal sense.<sup id="cite_ref-mmns_1-1" class="reference"><a href="#cite_note-mmns-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> For instance, the validity of the output proof may be more apparent to human users than the correctness of the algorithm, or a checker for the proof may be more amenable to <a href="Formal_verification" title="Formal verification">formal verification</a>.<sup id="cite_ref-mmns_1-2" class="reference"><a href="#cite_note-mmns-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup>

</p><p>Implementations of certifying algorithms that also include a checker for the proof generated by the algorithm may be considered to be more reliable than non-certifying algorithms. For, whenever the algorithm is run, one of three things happens: it produces a correct output (the desired case), it detects a bug in the algorithm or its implication (undesired, but generally preferable to continuing without detecting the bug), or both the algorithm and the checker are faulty in a way that masks the bug and prevents it from being detected (undesired, but unlikely as it depends on the existence of two independent bugs).<sup id="cite_ref-mmns_1-3" class="reference"><a href="#cite_note-mmns-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading2"><h2 id="Examples">Examples</h2></div>

<p>Many examples of problems with checkable algorithms come from <a href="Graph_theory" title="Graph theory">graph theory</a>.

For instance, a classical algorithm for testing whether a graph is <a href="Bipartite_graph" title="Bipartite graph">bipartite</a> would simply output a Boolean value: true if the graph is bipartite, false otherwise. In contrast, a certifying algorithm might output a <a href="Graph_coloring" title="Graph coloring">2-coloring</a> of the graph in the case that it is bipartite, or a <a href="Cycle_(graph_theory)" title="Cycle (graph theory)">cycle</a> of odd length if it is not. Any graph is bipartite if and only if it can be 2-colored, and non-bipartite if and only if it contains an odd cycle. Both checking whether a 2-coloring is valid and checking whether a given odd-length sequence of vertices is a cycle may be performed more simply than testing bipartiteness.<sup id="cite_ref-mmns_1-4" class="reference"><a href="#cite_note-mmns-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup>

</p><p>Analogously, it is possible to test whether a given <a href="Directed_graph" title="Directed graph">directed graph</a> is <a href="Directed_acyclic_graph" title="Directed acyclic graph">acyclic</a> by a certifying algorithm that outputs either a <a href="Topological_sorting" title="Topological sorting">topological order</a> or a directed cycle. It is possible to test whether an undirected graph is a <a href="Chordal_graph" title="Chordal graph">chordal graph</a> by a certifying algorithm that outputs either an elimination ordering (an ordering of all vertices such that, for every vertex, the neighbors that are later in the ordering form a <a href="Clique_(graph_theory)" title="Clique (graph theory)">clique</a>) or a chordless cycle. And it is possible to test whether a graph is <a href="Planar_graph" title="Planar graph">planar</a> by a certifying algorithm that outputs either a planar embedding or a <a href="Kuratowski's_theorem" title="Kuratowski's theorem">Kuratowski subgraph</a>.<sup id="cite_ref-mmns_1-5" class="reference"><a href="#cite_note-mmns-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup>

</p><p>The <a href="Extended_Euclidean_algorithm" title="Extended Euclidean algorithm">extended Euclidean algorithm</a> for the <a href="Greatest_common_divisor" title="Greatest common divisor">greatest common divisor</a> of two integers <span class="texhtml mvar" style="font-style:italic;">x</span> and <span class="texhtml mvar" style="font-style:italic;">y</span> is certifying: it outputs three integers <span class="texhtml mvar" style="font-style:italic;">g</span> (the divisor), <span class="texhtml mvar" style="font-style:italic;">a</span>, and <span class="texhtml mvar" style="font-style:italic;">b</span>, such that <span class="texhtml"><i>ax</i> + <i>by</i> = <i>g</i></span>. This equation can only be true of multiples of the greatest common divisor, so testing that <span class="texhtml mvar" style="font-style:italic;">g</span> is the greatest common divisor may be performed by checking that <span class="texhtml mvar" style="font-style:italic;">g</span> divides both <span class="texhtml mvar" style="font-style:italic;">x</span> and <span class="texhtml mvar" style="font-style:italic;">y</span> and that this equation is correct.<sup id="cite_ref-mmns_1-6" class="reference"><a href="#cite_note-mmns-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup>

</p>

<ul><li><a href="Sanity_check" title="Sanity check">Sanity check</a>, a simple test of the correctness of an output or intermediate result that is not required to be a complete proof of correctness</li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFMcConnellMehlhornNäherSchweitzer2011" class="citation cs2">McConnell, R.M.; <a href="Kurt_Mehlhorn" title="Kurt Mehlhorn">Mehlhorn, K.</a>; Näher, S.; Schweitzer, P. (May 2011), "Certifying algorithms", <i>Computer Science Review</i>, <b>5</b> (2): <span class="nowrap">119–</span>161, <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2Fj.cosrev.2010.09.009">10.1016/j.cosrev.2010.09.009</a></cite>.</span>

</li>

<li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text"><cite id="CITEREFAlkassarBöhmeMehlhornRizkallah2013" class="citation cs2">Alkassar, Eyad; Böhme, Sascha; <a href="Kurt_Mehlhorn" title="Kurt Mehlhorn">Mehlhorn, Kurt</a>; Rizkallah, Christine (June 2013), "A Framework for the Verification of Certifying Computations", <i><a href="Journal_of_Automated_Reasoning" title="Journal of Automated Reasoning">Journal of Automated Reasoning</a></i>, <b>52</b> (3): <span class="nowrap">241–</span>273, <a href="ArXiv_(identifier)" class="mw-redirect" title="ArXiv (identifier)">arXiv</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://arxiv.org/abs/1301.7462">1301.7462</a></span>, <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2Fs10817-013-9289-2">10.1007/s10817-013-9289-2</a></cite>.</span>

</li>

</ol></div></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2024-01-22" href="https://en.wikipedia.org/wiki/?title=Certifying_algorithm&oldid=1198007218">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>